00100	5. The behavior of the Christian and the lion is expressible by the 
00200	following algolish program:
00300	
00400	loop:	if x=y then go to eat;
00500		x ← if pc1(x,y) then c1(x) else if pc2(x,y) then c2(x) else c3(x);
00600		y ← if pl1(x,y) then l1(y) else if pl2(x,y) then l2(y) else l3(y);
00700		go to loop;
00800	eat:
00900	
01000		This program will fail to terminate if there exist predicates
01100	π1(x,y), π2(x,y), and π3(x,y) satisfying the conditions
01200	
01300	(i)	π1(a,b)
01400	
01500	(ii)	∀xy . π1(x,y) ⊃ x ≠ y ∧ π2(x,y)
01600	
01700	(iii)	∀xy . π2(x,y) ⊃ π3(if pc1(x,y) then c1(x)
01800				else if pc2(x,y) then c2(x)
01900				else c3(x),y)
02000	
02100	(iv)	∀xy . π3(x,y) ⊃ π1(x,if pl1(x,y) then l1(y)
02200				else if pl2(x,y) then l2(y)
02300				else l3(y))
02400	
02500	Therefore the program will terminate at %eat% if there do not exist
02600	such predicates which will be true if
02700	
02800		E ∧ F ⊃ ¬{π1(a,b) ∧
02900			[∀xy . π1(x,y) ⊃ x ≠ y ∧ π2(x,y)]
03000					∧
03100			[∀xy . π2(x,y) ⊃ π3(if pc1(x,y) then c1(x)
03200					else if pc2(x,y) the c2(x)
03300					else c3(x),y)]
03400					∧
03500			[∀xy . π3(x,y) ⊃ π1(x,if pl1(x,y) then l1(y)
03600					else if pl2(x,y) then l2(y)
03700					else l3(y))]}
03800	
03900	is a valid formula of first order logic.  (If the reader is annoyed
04000	by the presence of conditional expressions in logical formulas they
04100	can be eliminated by distributing the predicates π2 and π3 into
04200	the conditional expressions and then replacing the resulting Boolean
04300	conditional expressions by expressions involving only ∧, ∨, and ¬.)
04400	
04500		b. This case is even simpler than the previous case; the
04600	Christian will escape if there are predicates π1, π2, and π3
04700	satisfying
04800	
05100	(i)	π1(a,b)
05150	
05200	(ii)	∀xy . π1(x,y) ⊃ x ≠ y ∧ π2(x,y)
05300	
05400	(iii)	∀xy . π2(x,y) ⊃ π3(c1(x),y) ∨ π3(c2(x),y) ∨ π3(c3(x),y)
05500	
05600	(iv)	∀xy . π3(x,y) ⊃ π1(x,l1(x)) ∧ π1(x,l2(y)) ∧ π1(x,l3(y)).
05700	
05800	and this gives rise to
05900	
06000		E ⊃ ¬{π1(a,b) ∧ [∀xy . π1(x,y) ⊃ x ≠ y ∧ π2(x,y)]
06100				∧
06200				[∀xy . π2(x,y) ⊃ π3(c1(x),y) ∨
06300					π3(c2(x),y) ∨ π3(c3(x),y)]
06400				∧
06500				[∀xy . π3(x,y) ⊃ π1(x,l1(y)) ∧
06600					π1(x,l2(y)) ∧ π1(x,l3(y))]}.
06700	
06800	as the condition for the catchability of the Christian.